Process Analysis Toolkit  (PAT) 3.5 Help  
5.3.1 Language Translation

The easiest way of creating a model checker is to create a syntax rewriter from a domain specific language to an existing language in PAT. This is only recommended if the domain language is less expressiveness than the existing languages.

Comparing with other tools, programming a language translator is straightforward in PAT. Because PAT has well-defined APIs for Specification facade class and module language constructs, users only need to create the Specification model and generate the language constructs objects using these APIs. For example, Specification class in CSP# module offers the interfaces to create global Variables, Channels, Processes and Assertions. This approach requires little interaction with PAT codes. Most importantly, the target language model is automatic generated from the Specification class, which can guarantee syntax correctness. The usefulness of this extension has been demonstrated by the build-in translator from Promela4 to CSP# [ZHAO10] and the translator from UML state diagram to CSP# [ZHANGL10].

However, sometimes this approach will be infeasible. For example, the translation may not be optimal if special domain specific language features are present. In addition, reflecting analysis results (e.g., showing the counterexample trace) back to the domain model is often non-trivial.


 
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.